ecl-trans-normal(x)
== let T,ks,i,g,h,a,e = x in 
== (x, y:T. Dec(x = y)) & (n:. h(n,i)) & finite-type(T) & sorted(e) & no_repeats(;e) 

latex

---

clarification:

ecl-trans-normal(x)
== let T,ks,i,g,h,a,e = x in 
== (x:T, y:T. Dec(x = y  T)) & (n:. h(n,i))
== & finite-type(T)
== & sorted(e)
== & no_repeats(;e) 

latex

Definitions	let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), Dec(P), x:A. B(x), , A, b, finite-type(T), P & Q, sorted(L), no_repeats(T;l),
FDL editor aliases	ecl-trans-normal